//2-SAT问题
//_2_satisfiability.cpp

//有n个党派，每个党派中都有2个成员
//现在从每个党派中选取一个成员组成一个n个成员的委员会，各个党派成员之间存在矛盾关系
//比如某两党(a0, a1)(b0, b1)中，a0与b0不合，则a0和b0不能同时参加委员
//判断是否存在一个方案使得委员会中没有不合的成员，若存在则求出该方案

//1)基础概念
//成员选择是2-SAT问题的典型应用场景，它可以抽象为拥有n个成员的集合s
//集合中所有成员都只能取0或1，且成员之间存在如下两种约束
//约束1：
//约束2：
//i)s[i] = 1 or s[j] = 1，即s[i]和s[j]中至少有一个取1，也记作s[i] or s[j]
//即当s[i] = 0时必须有s[j] = 1，当s[j] = 0时必须有s[i] = 1
//考虑a0和b0不合，即a0和b0不能同时参加委员会
//即not(a = 0 and b = 0)，也记作not(a0 and b0)
//关系not(a = 0 and b = 0) 可以转为 (not a = 0) or (not b = 0) 再转为 a = 1 or b = 1
//即a1或b1参加委员会即可(也可a1和b1都参加)，将a0和b0映射为取0值，a1和b1映射为取1值
//则有s[a] = 1 or s[b] = 1，和s[i] = 1 or s[j] = 1完全相同
//当a0参加时必须b1参加，当b0参加时必须a1参加
//即当s[a] = 0时必须有s[b] = 1，当s[b] = 0时必须有s[a] = 1
//
//ii)类似的还可以有s[i] = 0 or s[j] = 0
//即s[i]和s[j]中至少有一个取0，也记作(not s[i]) or (not s[j])
//对应a1和b1不合的情况
//
//iii)还可以有s[i] = 0 or s[j] = 1
//即s[i] = 0和s[j] = 1中至少出现一个，也记作(not s[i]) or s[j]
//即当s[i] = 1时必须有s[j] = 1(s[i]不满足条件，则s[j]必须满足才能使or成立)
//当s[j] = 0时必须有s[i] = 0，该情况与前两个有些不同，还可以有其他可能但推导方式不变
//
//给出这样的多组约束，判断并求出一个满足所有约束的取值方案就称为2-SAT问题
//当约束2中可以涉及多个元素s[i]  = 1 or s[j] = 1 or s[k] = 1...
//该问题扩展为一个一般性的SAT问题，是NP完全问题
//
//2)构造有向图
//构造有2n个节点的有向图，即n对节点，每对节点分为i0和i1，对应s[i] = 0和s[i] = 1
//一对节点必须且只能选取一个，对于约束s[i] = 1 or s[j] = 1
//即当s[i] = 0时必须s[j] = 1，当s[j] = 0时必须s[i] = 1
//在有向图中添加从节点i0到j1的边e(i0, j1)和从节点j0到i1的边e(j0, i1)
//表示两节点间必须的关系
//对应的a1 or b1，当a0时必须有b1，当b0时必须有a1，将a映射为节点对i，b映射为节点对j
//在有向图中添加边的方式和集合s中取0和1的方式完全相同
//其他所有关系都可以按照这个方式添加边，最终得到一个有向图
//该有向图中可能存在不连通的节点和环
//
//3)原始解法
//在有向图中遍历所有节点对i，重复以下步骤
//若该节点对i尚未确定选取哪个，则任选其中一个
//假设选取了节点i0，则查看i0是否有一条指向节点j0或j1的边e(i0, j0)或e(i0, j1)
//边e(i0, j0)指代当选取节点i0时必须选节点j0，即当s[i] = 0时必须有s[j] = 0
//可能是这样的约束s[i] = 1 or s[j] = 0，当s[i] = 0没有满足条件时必须有s[j] = 0满足
//再映射为i1或j0两人参加委员会(也可i1和j0都参加)，即i0和j1二人不合
//则沿着选取的i0的边一直这样dfs推导下去，若不存在冲突情况，即可得到一个取值方案
//若产生冲突情况则选取另一个节点i1再进行dfs，若两个节点都存在冲突情况则不存在方案
//
//4)强连通分支解法
//考虑这样的约束，a1和b1不合，a0和b0也不合
//对应的数学模型是not(a1 and b1)，not(a0 and b0)
//即s[a] = 0 or s[b] = 0，s[a] = 1 or s[b] = 1
//当s[a] = 1时必须s[b] = 0，当s[b] = 1时必须s[a] = 0
//当s[a] = 0时必须s[b] = 1，当s[b] = 0时必须s[a] = 1
//在有向图中有边e(a0, b1)，e(b1, a0)，e(a1, b0)和e(b0, a1)
//即a0与b1，a1与b0形成了两个环，每个环都是最简单的只有两个节点的环
//这样特殊的约束条件使得有向图中出现环，也可能出现多个节点的环
//进一步环中一个节点若被选取，则该环的所有节点都必须被选取，且环是一个强连通分支
//
//先通过强连通分支算法先求出该有向图的所有强连通分支
//遍历有向图的所有节点对i，若i0和i1同属于一个环，则不存在取值方案满足所有约束
//若存在取值方案，由于2-SAT问题的约束总是
//使一对节点i0和i1分别属于两个环，并且这两个环的结构完全相同，或称对称的环
//将有向图中的所有环都看作一个节点，称为缩点，该操作使得新的有向图中不存在环
//注意将i0节点所在的环转化为一个缩点，假设该环被转化为节点c0
//对应的一定有i1节点所在的环也转化为一个缩点，假设被转化为节点c1
//按照新有向图的拓扑顺序遍历每个节点i，重复以下步骤
//若当前节点i未被染色，则将它染成蓝色，而将节点i对应的那个环染成红色
//若节点i是c0，则对应那个节点即为c1，这两个对称的节点必须染成不同颜色
//然后从节点c0和c1开始dfs，递归的将它们的所有邻边的节点也染成自己的颜色
//也可能出现孤立的节点，它在有向图中的拓扑顺序在最前面，不过该节点并不影响dfs遍历
//当图中所有节点都被染色后，即可得到蓝色和红色两种取值方案
//
//本问题使用到的技术有强连通分支，深度优先搜索，缩点和拓扑排序
//
//本文引用了“由对称性解2-SAT问题(百度文库)”，作者“351357741”
//“2-SAT解法浅析(百度文库)”，作者“华中师大一附中 赵爽”

//bool _2_satisfiability(graph_list g, int n, int *s)
